﻿// Jinx AJAX Framework
// Copyright (C) 2008 Blake Hegerle
//
// This program is free software: you can redistribute it and/or modify
// it under the terms of the GNU General Public License as published by
// the Free Software Foundation, either version 3 of the License, or
// (at your option) any later version.
//
// This program is distributed in the hope that it will be useful,
// but WITHOUT ANY WARRANTY; without even the implied warranty of
// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
// GNU General Public License for more details.
//
// You should have received a copy of the GNU General Public License
// along with this program.  If not, see <http://www.gnu.org/licenses/>.

using System;
using System.Collections.Generic;
using System.Linq;
using Formality.Levels;
using Formality.FormalSystem;

namespace Formality.Game
{
    public class ProofChecker<T>
        where T : class
    {
        private readonly List<string> BadProofs;
        private readonly string Name;
        private readonly Func<string, T> Parser;
        private readonly IEnumerable<Sentence<T>> Problems;
        private readonly Func<T, IEnumerable<Sentence<T>>, bool> Reasoner;
        private readonly bool ShowTrace;

        public ProofChecker(string Name, Func<string, T> Parser, Func<T, IEnumerable<Sentence<T>>, bool> Reasoner,
                            bool Trace)
        {
            ShowTrace = Trace;
            this.Name = Name;
            this.Reasoner = Reasoner;
            this.Parser = Parser;

            BadProofs = new List<string>();

            Problems = new FullEnumerator<T>(Parser);
        }

        public IEnumerable<string> Failures
        {
            get { return BadProofs; }
        }

        private IEnumerable<string> AllProblemIds
        {
            get { return from S in Problems select S.Id; }
        }

        public bool Check()
        {
            var Player = new DurablePlayer<Proposition>(Name);

            foreach (var Problem in Problems)
            {
                Trace("----------------------");
                Trace("Checking " + Problem.Id + " " + Problem.Item);
                Trace("----------------------");

                var Submissions = Player.ProblemSubmissions(Problem.Id).ToArray();

                if (Submissions.Length < 1) continue;
                if (!Check(Submissions, Problem))
                    BadProofs.Add(Problem.Id);
            }

            return BadProofs.Count == 0;
        }

        private bool Check(IEnumerable<string> Submissions, Sentence<T> Problem)
        {
            var Premises = new List<Sentence<T>>(GetPremises(Problem.Id));

            foreach (var Submission in Submissions)
            {
                T Proposition;

                try
                {
                    Proposition = Parser(Submission);
                }
                catch (Exception)
                {
                    Trace("Could not find a proposition: " + Submission);
                    continue;
                }

                if (Reasoner(Proposition, Premises))
                {
                    if (Proposition.Equals(Problem.Item))
                    {
                        Trace("Can infer the goal: " + Proposition);
                        return true;
                    }

                    Trace(Proposition);
                    Premises.Add(new Sentence<T>("Sub", null, Proposition));
                }
                else
                {
                    Trace("Cannot infer " + Proposition);
                }
            }

            return false;
        }

        private void Trace(object o)
        {
            if (ShowTrace)
                Console.WriteLine(o);
        }

        private IEnumerable<Sentence<T>> GetPremises(string Id)
        {
            return Problems.TakeWhile(P => P.Id != Id);
        }
    }
}